-
Notifications
You must be signed in to change notification settings - Fork 143
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Monoid theory moved from examples/algebra to src/algebra (core library) #1224
Conversation
…m examples/algebra/monoid/README.md)
On a second thought, the name change of |
Per our offline discussions, the new files under |
Thanks! |
commit 2d2cddffe3dfeee7bc31b0fb499fb32cd2218dd2 Author: Chun Tian (binghe) <[email protected]> Date: Mon Jun 3 10:42:43 2024 +1000 Updated CCS example commit f037e2c003269ba2d30ec185263b21be93d09a6b Author: Chun Tian (binghe) <[email protected]> Date: Thu Jun 6 16:29:23 2024 +1000 Move simple_assert to Lib commit 0c39a0cfc34249e1315e8a75b399d6ca52892e96 Author: Chun Tian (binghe) <[email protected]> Date: Thu Jun 6 11:09:55 2024 +1000 Further cleanup of hurdUtils (assert -> simple_assert) commit a1037385a92acdb9b8bb1f0c243fe6f1f6120eaf Author: Michael Norrish <[email protected]> Date: Mon Jun 3 10:48:36 2024 +1000 Fix examples/vector given changes in 562bb668f092d commit 1253e33fc97a9b4a28a55fc8b924787228823128 Author: Michael Norrish <[email protected]> Date: Fri May 31 14:16:11 2024 +1000 Use correct Hungarian accent in Kőnig Lemma comment My googling suggests that oe is an acceptable ASCII-only rendering of this so keeping the theorem names as koenig_lemma etc is reasonable. commit b9b2a68456b383cd20d3274ce454e41d3aded764 Author: Michael Norrish <[email protected]> Date: Thu May 30 15:43:26 2024 +1000 Expose the resolution "primitive" behind resolve_then resolve_then requires the output of the resolution to be passed to a theorem-tactic (and will backtrack if the theorem-tactic fails with a HOL_ERR); the new gen_resolve_then will pass to any consumer/continuation, backtracking if *that* fails with a HOL_ERR. The old resolve_then is then an easy instance of the new function. commit 495e1a75b0754cb446be4f541f74a97793d5e01f Author: someplaceguy <[email protected]> Date: Thu May 30 17:25:08 2024 +0000 HolSmt: initial support for the exponential function This initial support is very limited and only consists in adding a couple of useful theorems to the proving context. Hopefully, in the future more extensive support is implemented by adding support for Z3's native power operator, which should allow HolSmt to prove a lot more goals. This implementation would need to be similar to the implementation of integer division, since it doesn't exactly match HOL4's exponential functions. The latter would also have a couple of limitations, namely: 1. it would only work for Z3, since this operator is a Z3 extension and not part of the SMT-LIB standard 2. proof reconstruction would not work commit 616c94b7ddcd2adfbad79343318f43b00bc43420 Author: someplaceguy <[email protected]> Date: Thu May 30 11:49:17 2024 +0000 HolSmt: add z3_tac and z3o_tac tactics These accept a list of theorems, like `metis_tac`. The free vars in the theorems are automatically quantified with `Drule.GEN_ALL` and added to the list of assumptions in the goal, prior to sending the goal to the SMT solver. This is needed to avoid any passed-in theorems to be specialized to free vars in the goal that happen to have the same name, which is almost always not what the user wants (and if the user really wants it, they can always assume such theorems manually if needed). This matches the behavior of `metis_tac`, thus avoiding unwanted surprises. commit 074d16fdb751d549474ba38d6fdc5ec6459d4107 Author: someplaceguy <[email protected]> Date: Thu May 30 11:43:16 2024 +0000 HolSmt: allow SMT solvers to peek under abbreviations Otherwise, they won't be able to see what the variables are being abbreviated to. This problem would cause some goals that can be solved with metis_tac[] to fail with HolSmt. The fix is to add the definition of the `Abbrev` symbol to the list of theorems that are added to the assumptions prior to calling the SMT solver. commit fe6fe549423e55e2832f56e083e7e12bc2edc37a Author: Chun Tian (binghe) <[email protected]> Date: Fri May 24 20:26:11 2024 +1000 FTBFS commit 596437ee577524ec54ad041b4ac2ee03b32bd3ca Author: Chun Tian (binghe) <[email protected]> Date: Fri May 24 20:12:20 2024 +1000 Fix Holmakefiles after moving iterateScript.sml out of src/real commit 562bb668f092de2446cc7ac63774abefecb9be8a Author: Chun Tian (binghe) <[email protected]> Date: Fri May 24 20:10:03 2024 +1000 Move out real-related theorems from iterateTheory commit 77d5e30d24ada01dbe89b0cdb1e2ef170111af99 Author: Chun Tian (binghe) <[email protected]> Date: Tue May 21 18:47:26 2024 +1000 [ringLib] RING_TAC|RULE ported from HOL-Light commit 7dc35fb6ea2e1a0b06e8a6cae7874529bcb913ed Author: Michael Norrish <[email protected]> Date: Fri May 24 17:05:27 2024 +1000 Git-ignore generated HTML in examples/generic_finite_graphs commit 1388e15fb1088eeef73064dd5214abd047a6e9c5 Author: Michael Norrish <[email protected]> Date: Fri May 24 17:04:38 2024 +1000 Remove unused entrypoints from hurdUtils; replace Cond with impl_tac commit 19857c9570c4db45bb6410a1ced45b9ab7bb4cb7 Author: Chun Tian (binghe) <[email protected]> Date: Wed May 22 13:13:19 2024 +1000 Fixed intLib to avoid noisy output; some cleanups in hurdUtils commit afa5534d968a4985a916a525e82f5ca0a8e96c26 Author: Michael Norrish <[email protected]> Date: Wed May 22 20:29:43 2024 +1000 Fix parsing issues with src/ring/src/EVAL_* These theories now get sucked into more theories because integerRingLib is also used more often. commit 8ccf8cf879f247fc664e907ade75d02f0f3ff681 Author: Johannes Åman Pohjola <[email protected]> Date: Wed May 22 11:57:31 2024 +1000 Modernise syntax for Turing machine example commit f6c3ef26dd757ab1e390c66ca90d4018a1405d79 Author: Chun Tian <[email protected]> Date: Tue May 21 16:45:32 2024 +1000 HOL-Light's INTEGER_TAC (#1238) * HOL-Light's INTEGER_TAC * Fix manual builds (by loading intLib earlier) * Fix trailing whitespaces... * Add some basic documentation about intLib.INTEGER_TAC|RULE * Fixed a bug in DISJ_ACI_RULE due to differences of UNDISCH between HOL4 and HOL-Light; fixed typo in next-release.md commit fe0e72dc46aa5ca62a9ec826c69bd7dfe8dc301d Author: Michael Norrish <[email protected]> Date: Thu May 16 17:08:33 2024 +1000 Define simultaneous substitution for lambda/basics/cterm Not all of term's theorems about its analogue have been ported across yet. commit c0974a790185ad6c0ab57589d4da0a7ddf2aa67e Author: Michael Norrish <[email protected]> Date: Thu May 16 14:52:16 2024 +1000 Automatically simplify numeral subtractions in ℝ Again, thanks to Eric Hall for the suggestion. commit 7cbe9f6db6d94b75561563e89ba2985496b58daf Author: Michael Norrish <[email protected]> Date: Thu May 16 14:24:32 2024 +1000 Make M-h M's output prettier with new Hol_pp.print_DBselection Previously, the emacs mode command just made a call to the DB function, which emitted a list of public_data values, which didn't appear as nicely as the output from M-h f. Thanks to Eric Hall for the suggestion. commit f0bc0d88e61776435fda60535bbb7d27f475bfc6 Author: Michael Norrish <[email protected]> Date: Wed May 15 16:49:38 2024 +1000 Document mapPartial in DESCRIPTION commit fbdc2552a0d2d017c021f461d1a4600bd44bc8fd Author: Michael Norrish <[email protected]> Date: Wed May 15 16:49:14 2024 +1000 Minor tweaks to DESCRIPTION's section on lists commit 24748e92c45d14387b97d38746721d4a47f91694 Author: Michael Norrish <[email protected]> Date: Wed May 15 15:09:58 2024 +1000 Define a mapPartial function in listTheory commit 38e543944dad6edf694219b16ea73b307e36c28a Author: Michael Norrish <[email protected]> Date: Tue May 14 16:39:33 2024 +1000 Get src/combin seltest to build with Holmake's tee command commit f0ad49c15e3e3b22db36c627016eb3710d88a236 Author: Michael Norrish <[email protected]> Date: Tue May 14 16:38:46 2024 +1000 [Holmake] Modify built-in tee to not create file if command fails commit 013b19590936441fbf63bcfc835c820d9692303b Author: Michael Norrish <[email protected]> Date: Tue May 14 15:45:41 2024 +1000 Create an INCLUDES line for Keccak example commit e780a0d412ea8ee8b61aec367e5481fe01d5d5f5 Author: Chun Tian <[email protected]> Date: Tue May 14 14:53:48 2024 +1000 Combined group and ring theories from examples/algebra to core library (#1235) * Move combined groupTheory and ringTheory to core library; HOL-Light compatible ringLibTheory * Fixed missing signature of TRANS_TAC; added ANTS_TAC ported from HOL-Light * FTBFS examples/algebra * Move ANTS_TAC from Tactic to liteLib (= impl_tac); fix builds of examples/algebra/ring commit 7f59049385c2a9152ae0477e99956d793742ef15 Author: rsoeldner <[email protected]> Date: Mon May 13 19:36:01 2024 +0200 add lowercase rewrite tactics commit 63d7fac140bb3dfbe3b7552e64a6d1ca5b522101 Author: Michael Norrish <[email protected]> Date: Tue May 14 14:44:54 2024 +1000 Get examples/Crypto/Keccak to build at selftest level 1 commit 7e24888d5914a492e9ff7eb44381247e9a33dc25 Author: Michael Norrish <[email protected]> Date: Tue May 14 14:39:34 2024 +1000 Delete redundant constant transfer$FUN_REL Use instead quotient$===>, which just needed to be made slightly more polymorphic. That additional polymorphism didn't break anything. commit b4a42012d90c2666475d53dc7a083125940738fc Author: rsoeldner <[email protected]> Date: Fri May 10 10:12:31 2024 +0200 add mk_bool commit 6862df4f5a490c21c4ca3515bcc4977d0c98856b Author: Michael Norrish <[email protected]> Date: Sat May 11 11:42:08 2024 +1000 Fix a broken INCLUDES line commit c612b6bbc55f0e00e60779dfade8d4eb908c56bc Author: Magnus Myreen <[email protected]> Date: Thu May 9 21:03:48 2024 +0200 Get Keccak to evaluate using cv_eval commit 142901f307ecb262f3dfa8ae7cae064c855f5efe Author: Magnus Myreen <[email protected]> Date: Thu May 9 10:00:19 2024 +0200 Get Keccak_{256,224} and SHA3_* functions translated commit 041ae75108845fd94f1ac462a3d46ed09d388524 Author: Ramana Kumar <[email protected]> Date: Mon May 6 07:30:40 2024 +0100 Prove cheat about LOG2 commit 944e7d0381b6e14d7c74bc553071191ad5c24916 Author: Ramana Kumar <[email protected]> Date: Sun May 5 23:29:12 2024 +0100 Add bool_lookup_def to the compset commit 0c7ee73248eaf2a0725e4e4ce47559decf1ccf6e Author: Ramana Kumar <[email protected]> Date: Sun May 5 23:28:50 2024 +0100 Add prefer_num() to avoid incorrect number parsing commit 0bd44a52fa41928e1e3c9dc7e8d3d172a2bcd9f4 Author: Ramana Kumar <[email protected]> Date: Sun May 5 23:28:20 2024 +0100 Remove THE (lookup ...) and to_bool_lookup commit af3529cf316e34a41fe0608a3f3e463276b7ec12 Author: Ramana Kumar <[email protected]> Date: Sun May 5 22:50:36 2024 +0100 Remove THE (lookup ...) from theta_spt_def commit c2b26fa2972e7d86cbd97ac29f501b9499b6bff4 Author: Magnus Myreen <[email protected]> Date: Fri May 3 00:27:19 2024 +0200 Translate most of Keccak functions (with a few cheats) commit 5730d611644cd504bd6c3af20b0e1412ada9bd8f Author: Magnus Myreen <[email protected]> Date: Thu May 2 19:16:29 2024 +0200 Translate toSortedAList commit a83ea7e32ce04efb928f38d1084c223f6333e272 Author: Michael Norrish <[email protected]> Date: Fri May 10 17:16:24 2024 +1000 Fix another developers manual typo commit fd7ceb496620624800d6f5599ae1fc121999b777 Author: Michael Norrish <[email protected]> Date: Fri May 10 17:12:33 2024 +1000 Set compile-command Local-var for emacs builds of developer manual commit a3167c8a098b10ea5fc79c2407030ecc293e424a Author: Michael Norrish <[email protected]> Date: Fri May 10 17:12:02 2024 +1000 Explain quote-filter is built-in with Poly/ML (not separate process) commit c873050eeced0f704c51a9a87ffb422bcae94dff Author: Michael Norrish <[email protected]> Date: Fri May 10 17:11:33 2024 +1000 Correct typos in Developers manual commit 46b102fc1653ea99e29d25979166e427a7e0a3ea Author: Michael Norrish <[email protected]> Date: Fri May 10 17:11:11 2024 +1000 Describe how build cleanall may be necessary when rebuilding commit bbad3fd57b603a1a4d079d738e45e97d5a71e834 Author: Michael Norrish <[email protected]> Date: Fri May 10 17:10:52 2024 +1000 Document upto-parallel sequence file commit d80a6972e7f87e6f44a3e978b7c4ca972a428c76 Author: Hrutvik Kanabar <[email protected]> Date: Wed May 8 10:00:43 2024 +0100 Move "print length" into `Globals` As per request from @mn200 commit 320e6790ea099f54ba74ea3c1b61460be75f5a97 Author: Hrutvik Kanabar <[email protected]> Date: Tue May 7 14:44:53 2024 +0100 Use "print lengths" in `monadsyntax` As suggested by @binghe commit e70c86e063a1a623ae5ed60554618a4d683bad48 Author: Hrutvik Kanabar <[email protected]> Date: Fri May 3 15:45:55 2024 +0100 Make `monadsyntax` more aware of print depth commit 07e09c5cb5582ed81b05a3fe75181c595fff4e39 Merge: 325162975 4b7d02179 Author: Michael Norrish <[email protected]> Date: Fri May 10 10:22:29 2024 +1000 Merge pull request #1224 from binghe/monoidTheory Monoid theory moved from examples/algebra to src/algebra (core library) commit 325162975c2778e5b1bc07c199b6f1f79b9304ae Author: Michael Norrish <[email protected]> Date: Mon May 6 12:45:07 2024 +1000 Fix bad reference to bootstrap example in parallel Holmakefile commit 6ef46c0a89323ec39ff2c2ec148d0034bbbd8d9f Author: Michael Norrish <[email protected]> Date: Mon May 6 12:39:56 2024 +1000 Fix Holmakefile bug causing unnecessary rebuilds By pointing the INCLUDES back at the already built src/num/theories/cv_compute, the files there get rebuilt (because of the implicit dependency on hol.state which will indeed be fresher). Then numheap and lots else gets rebuilt in turn. Basically the same thing I fixed in 12c611b12123. commit 0090fcd26df521f3deb63bf9cf0ef9c54f2cf9ac Author: Michael Norrish <[email protected]> Date: Mon May 6 12:06:38 2024 +1000 Get developers/genUseScript to compile again (still wrong though) commit c75093f7a9bdf34fb10002e1e50e0a0c1ec153fc Author: Chun Tian (binghe) <[email protected]> Date: Sat May 4 00:00:57 2024 +1000 FTBFS (NOT_ZERO is from "examples/algebra") commit 865dbda999616b1f65a036055f0bfdbd1b0576e1 Author: Chun Tian <[email protected]> Date: Fri May 3 23:33:22 2024 +1000 Update docker-ci.yml commit 36d0b54855455d80bb7b61074495e31b75922a9c Author: Chun Tian <[email protected]> Date: Fri May 3 23:32:56 2024 +1000 Update docker-ci-for-pr.yml commit 3fa1d37aa6ea8275d4dc7ac579bd750862c2b3c4 Author: Chun Tian (binghe) <[email protected]> Date: Fri May 3 23:30:13 2024 +1000 Fixed --otknl build (up to hol-base / boss) using old Arithconv.sml commit 6c43d903d149104e34294be8ac0893a25ec24fd8 Author: Chun Tian (binghe) <[email protected]> Date: Sun Apr 28 12:56:10 2024 +1000 Some wording fixes in TRANS_TAC.doc commit e87d28cfab3b0aa611edef74c7785807ffe0c873 Author: Chun Tian (binghe) <[email protected]> Date: Sat Apr 27 12:26:15 2024 +1000 TRANS_TAC ported from HOL-Light commit 4b7d021796670f412b0423ef4465ef3453d92096 Author: Chun Tian (binghe) <[email protected]> Date: Fri May 3 13:33:10 2024 +1000 FTBFS (help) commit e6ce07231667c75940e69090d0a4c5aea1700a8c Author: Chun Tian (binghe) <[email protected]> Date: Fri May 3 11:47:11 2024 +1000 Move new files into subdirectories under src/algebra commit 4387c34e4a1d0a578c04b759fe735a6dc08f2dda Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 30 18:49:16 2024 +1000 Fixed building HOL manuals with PolyML (and not in --otknl) commit 27e4453054f20589111f618f94dd065085b5e6b4 Author: Chun Tian (binghe) <[email protected]> Date: Thu Apr 25 21:09:27 2024 +1000 FTBFS with Moscow ML commit 675fcb139002ecf5f62b9f68e95872954da652b9 Author: Chun Tian <[email protected]> Date: Thu Apr 25 18:43:34 2024 +1000 Update docker-ci.yml (add build-mosml) commit 79a0a60484ceb97c9ad3a72b91bcb655aaa39c50 Author: Chun Tian <[email protected]> Date: Thu Apr 25 18:42:55 2024 +1000 Update docker-ci-for-pr.yml (added build-mosml) commit 82a9c2d8dfade24e2caa5513ba782d04dabc2f3c Author: Chun Tian (binghe) <[email protected]> Date: Thu Apr 25 18:40:21 2024 +1000 Updated Dockerfiles with necessary TeXlive packages for building HOL manuals commit e006edd4c63dd1e725e8e19b18807bb13f96db1e Author: Michael Norrish <[email protected]> Date: Tue Apr 30 15:49:59 2024 +1000 Fix bug in cv_typeLib (translation failed in limited grammar ctxts) Bug reported by “someplaceguy” on CakeML discord, giving the name for the regression test script. Library code was calling the global parser, which as we all know is a mortal sin. commit 02a954437bfe96f7ba8b3f7f9271a680f441d927 Merge: a4084dad4 81398409d Author: Chun Tian (binghe) <[email protected]> Date: Thu Apr 25 20:45:55 2024 +1000 Merge remote-tracking branch 'origin/develop' into monoidTheory commit 81398409d1dbb6e695c0df0a4e40be075fdd0477 Author: Michael Norrish <[email protected]> Date: Thu Apr 25 22:16:05 2024 +1200 Produce new blank next-release.md file for what I assume will be T-2 commit fd366fde86123cf8d42ca2530fa10c15fbf14549 Merge: 6dbb43de3 2d798aea0 Author: Michael Norrish <[email protected]> Date: Thu Apr 25 22:13:47 2024 +1200 Merge tag 'trindemossen-1' into develop commit 2d798aea036cf23fe3f5b6ce5f939cb491a07119 Author: Magnus Myreen <[email protected]> Date: Tue Apr 23 10:16:35 2024 +0100 Fix typo in the Description commit 6dbb43de313fcb6db93fd69adce21ed024b76590 Author: Magnus Myreen <[email protected]> Date: Tue Apr 23 10:16:35 2024 +0100 Fix typo in the Description commit a4084dad40e8cc7e339ef97a149dcccd877b6ea1 Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 23 11:21:43 2024 +1000 FTBFS examples/lambda commit 2da4265c965ef3ad80e39255b48657eb18e71210 Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 23 10:31:06 2024 +1000 Revert name changes of SNOC_LAST_FRONT for better backward compatibility commit 112b2b69bb3f8b1b03f66f1a7ffe362b755ebc67 Author: Michael Norrish <[email protected]> Date: Mon Apr 22 16:48:19 2024 +1000 Stamp current release notes as what's going into next release commit 12c5f2ef701ef39c457840d4980b9af64392dcab Author: Chun Tian (binghe) <[email protected]> Date: Mon Apr 22 05:07:05 2024 +1000 Mention new algebra theories in next-release.md (using some words from examples/algebra/monoid/README.md) commit 4630435c969379dc681d26c9243642fe1754641f Author: Chun Tian (binghe) <[email protected]> Date: Mon Apr 22 04:19:06 2024 +1000 Fixes of examples/lambda work due to one renamed theorem in rich_listTheory commit d9c43039ffbc18492acec03e554caabc07f737c4 Author: Chun Tian (binghe) <[email protected]> Date: Mon Apr 22 03:45:18 2024 +1000 Changes of examples/{AKS|fermat|simple_complexity} after src/algebra/monoidThoery commit 6bd26f377211aafc174add159bb12258fe0646a7 Author: Chun Tian (binghe) <[email protected]> Date: Sun Apr 21 20:53:28 2024 +1000 Algebra materials moved to core theories (up to monoid) commit 12c611b12123da645e2d6dc86f640fe6cf52a981 Author: Michael Norrish <[email protected]> Date: Fri Apr 19 22:16:28 2024 +1000 Fix Holmakefile INCLUDES error causing unnecessary HOL rebuilds You can't link back to src/ directories that precede boss because the system imagines that the source files there depend on hol.state and will promptly rebuild/recompile them, causing headaches later. commit ef4c2c8c2f864b9de0079ff61299cdc6acc74964 Author: Anthony Fox <[email protected]> Date: Thu Apr 18 14:59:12 2024 +0100 Rework IN_CONV implementation IN_CONV (used by EVAL) was suffering from performance issues related to excessive recursion (triggered through a "handle HOL_ERR _" that has been removed in the reworked version). In particular, IN_CONV was not working well for terms of the form: x1 INSERT x2 INSERT ... xn INSERT { y | P y } commit 244c07da3e8592a9c4b1754a2c93c83f0da5759e Author: Michael Norrish <[email protected]> Date: Thu Apr 18 17:17:44 2024 +1000 Fix test broken by arrival of rationals into dependencies commit 2dc54739f1fe5c0e2111b2b31c2d4a3953cc7f65 Author: Michael Norrish <[email protected]> Date: Wed Apr 17 13:44:46 2024 +1000 Add INCLUDES line to bootstrap/Holmakefile to ensure parallel build As the dependency cv_transLib is also being built in parallel, the INCLUDES line is needed so that this directory is not attempted until cv_transLib is built. commit 4fa4503bce3a147a36fbbfbd5ff7f96c61085c8d Author: Michael Norrish <[email protected]> Date: Wed Apr 17 13:27:20 2024 +1000 Adjust Holmake/theory-diagnostics to distinguish --fast from cheat commit 81a7c2fd31c4a52cce0b34f0bf3841b54cf1edbe Merge: 76ecb1d3d 7d8de5ca8 Author: Michael Norrish <[email protected]> Date: Tue Apr 16 15:22:42 2024 +1000 Merge pull request #1217 from HOL-Theorem-Prover/cv_translator cv translator commit 7d8de5ca85588eb33fdfef5ccbae43337ef21704 Merge: 009088e4a 76ecb1d3d Author: Michael Norrish <[email protected]> Date: Tue Apr 16 15:21:14 2024 +1000 Merge branch 'develop' into cv_translator commit 76ecb1d3d4baae7343a97ebca2efc579346e08cc Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 9 20:26:11 2024 +1000 More primitive definition of q_set (IMAGE real_of_rat UNIV) commit 4291f88cd08bcff4dfb445b94219819cd9e8d00c Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 9 17:11:14 2024 +1000 Attempt to fix dining_criptosTheory by deprecating int/rat commit 25f45dd9f13bab5ede6f174cf1f1f46a52443961 Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 9 15:35:01 2024 +1000 Fix probability-related code after loading real_of_ratTheory by deprecating int and rat in term parser commit 5adf5d00209d3b8bb7823571508df0f2a4eef395 Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 9 15:33:00 2024 +1000 Move q_set (real_rat_set_def) theorems from real_sigma to real_of_rat with duplicated proofs merged commit e444dac45648885502641cd58deb351d0801121a Author: Chun Tian (binghe) <[email protected]> Date: Tue Apr 9 15:03:20 2024 +1000 [gcd,rat] theorems cherry-picked from the ongoing `cv_translator` branch (#1217) commit 009088e4a9f26128af32d89a009bbaa54fd39480 Author: Hrutvik Kanabar <[email protected]> Date: Fri Apr 12 00:04:00 2024 +0100 Try to fix regression commit 4a79f07297aa0df05b94f1b10830f7dea7ee242d Author: Hrutvik Kanabar <[email protected]> Date: Thu Apr 11 23:12:47 2024 +0100 Fix a failing selftest commit 6300798eaa05829e57d241ed36509d01cc4bcdae Author: Hrutvik Kanabar <[email protected]> Date: Thu Apr 11 22:44:47 2024 +0100 Uncheat cv translation in `examples/bootstrap` commit 6d82d9940a51ba8f467b43b8347212f335c1489a Author: Magnus Myreen <[email protected]> Date: Thu Apr 11 07:37:10 2024 +0200 Fix a silly mistake in a cv_rep theorem commit c297f94baeb53125e52a010f9b9659690241c944 Author: Magnus Myreen <[email protected]> Date: Thu Apr 11 05:04:58 2024 +0200 Replace cv_sum_depth by cv_size (and delete cv_size_alt) commit d2705cdc3fbddeaba656c955cab45b983c10dc28 Author: Magnus Myreen <[email protected]> Date: Thu Apr 11 04:45:53 2024 +0200 Remove references to examples/bootstrap from examples/cv_compute commit 1bc19e5b6cbb475ffca62ef85aa75fcc6a578372 Author: Magnus Myreen <[email protected]> Date: Thu Apr 11 04:14:40 2024 +0200 Use cv_eval instead of EVAL Note that this commit leaves a cheat that needs removing. commit 4c9b707ee09fa5cfedca6cfb6ebb91a371a8b447 Author: Michael Norrish <[email protected]> Date: Thu Apr 11 09:20:47 2024 +1000 Fix proof failure caused by name generation change in 68ea515ce46a83 commit 3f0b36ca4c7c5d22459b0058ccb5452858d38a72 Author: Michael Norrish <[email protected]> Date: Wed Apr 10 22:00:55 2024 +1000 Simplify transfer approach for monoids as types theory Vast majority of theorems transfer cleanly commit 68ea515ce46a835a7086934dc099ebf02b5ec5fa Author: Michael Norrish <[email protected]> Date: Wed Apr 10 21:56:11 2024 +1000 Improve transferLib's choices for bound names (mimick source) commit 4fbc78b13a185c10c1f054e79a41611c7318dcc0 Author: Michael Norrish <[email protected]> Date: Tue Apr 9 18:24:34 2024 +1000 Transfer more theorems semi-automatically to monoid as type theory commit d27435acb96c050da315dd65676f0eaeb131a3c3 Author: Michael Norrish <[email protected]> Date: Tue Apr 9 18:23:43 2024 +1000 Sequence file to build core HOL up to point of parallelisation commit 190392c28bd3f7aa723f97f973b8f575d999ecf0 Author: Chun Tian (binghe) <[email protected]> Date: Sat Mar 23 17:38:45 2024 +1100 Fix uses of newtypeTools.rich_new_type in newly committed work commit 4ec64bcc562d36bcceaec7e84097b7ddea18bc15 Author: Chun Tian (binghe) <[email protected]> Date: Fri Mar 22 12:56:37 2024 +1100 FTBFS rich_new_type{} in nomdatatype.ml commit b9335aa4a16a20ada0af10816f16f345ad340e3d Author: Chun Tian (binghe) <[email protected]> Date: Fri Mar 22 12:34:59 2024 +1100 More arguments (ABS, REP) of newtypeTools.rich_new_type commit 84f2039b4b5161d752a757f7dbff0874ca65aebd Author: someplaceguy <[email protected]> Date: Sat Mar 23 19:58:36 2024 +0000 HolSmt: remove workaround for #1203 Now that all known issues were fixed wrt. ARITH_PROVE not proving goals that COOPER_PROVE could, we can remove this workaround, thus making proof replay faster in some cases. commit 70bec8c55cc072390806fc27ee3ff146c544b378 Author: someplaceguy <[email protected]> Date: Mon Mar 18 17:37:50 2024 +0000 HolSmt: parse `assign-bounds` index in arith rules This commit fixes a parsing error when parsing arithmetic `th-lemma` inference rules with an `assign-bounds` parameter, i.e.: ((_ th-lemma arith assign-bounds ...) ...) The error was due to `assign-bounds` not being in the known term dictionary. commit aee048a87d352226c758752e354bdcd769a18ce9 Author: someplaceguy <[email protected]> Date: Mon Mar 18 17:16:41 2024 +0000 HolSmt: handle end-of-stream when parsing SMT-LIB files The SMT-LIB file parser was ending up raising an end-of-stream exception unless the `(exit)` command was present in the SMT-LIB file, even though the `(exit)` command does not seem to be mandatory according to the SMT-LIB v2.6 standard. commit d4ab50df4c6ec588aa998aa5490710d18b39e7cb Author: someplaceguy <[email protected]> Date: Mon Mar 18 15:28:46 2024 +0000 HolSmt: parse `declare-const` commands Add support for parsing `declare-const` commands to the SMT-LIB parser. commit 819ce3c3bafbf447bc46d97575447cd3fea088df Author: someplaceguy <[email protected]> Date: Sun Mar 17 11:38:58 2024 +0000 HolSmt: don't get rid of `quot` and `rem` in arithmetic rules It should not be necessary to rewrite these symbols with their definitions, because from the perspective of SMT solvers, these should just be functions like any others. Therefore, when replaying arithmetic proof steps, the proof handler should not need to understand what `quot` and `rem` are. This is a partial revert of the following commit: 6220a17848fd58bcb54bb9df9df6b55d5859abf0 It's not clear to me why I introduced this change in the first place, since the tests do work fine without it. Also, there doesn't seem to be any performance regression. commit b8fa4ad3ffa7453a6f6cb2d49473224daff5b4c2 Author: someplaceguy <[email protected]> Date: Fri Mar 15 12:01:30 2024 +0000 HolSmt: ignore indices in `rewrite` proof rules In case `rewrite` proof rules ever come to have indices, let's ignore them instead of erroring out. commit 391faf850d46b9de4e09de6478e451ec87984a29 Author: someplaceguy <[email protected]> Date: Thu Mar 14 17:21:12 2024 +0000 HolSmt: add `let`, `ediv` and `emod` simps to `thm_AUTO` commit 055488c99a8a7c9dd7827c9e069dcaf87370f9e7 Author: someplaceguy <[email protected]> Date: Thu Mar 14 16:48:01 2024 +0000 HolSmt: add full battery of `quot` and `rem` tests commit 1a87909fc794783df8f1262ed73c5d8ff2fa2619 Author: someplaceguy <[email protected]> Date: Thu Mar 14 16:13:25 2024 +0000 HolSmt: replay goals containing `quot` and `rem` HOL4's integer arithmetic decision procedures cannot handle `quot` and `rem`, so proof steps containing these symbols were failing to replay. This commit rewrites goals containing these symbols to increase the chances of a successful replay. `thm_AUTO` was similarly improved, as it had the same limitation and was failing to prove some of the self-tests. commit 23af0d085f12415cfb179d54e647c3c878c1a916 Author: someplaceguy <[email protected]> Date: Thu Mar 14 12:28:42 2024 +0000 HolSmt: remove workaround for NotFound exn in ARITH_TAC Now that #1209 is fixed, we can remove the workaround for it in HolSmt. commit 72f09bbbae2e181e7fbab38c773e19ab87cbc8ea Author: someplaceguy <[email protected]> Date: Thu Mar 14 12:25:37 2024 +0000 HolSmt: use integerTheory's ediv and emod Now that integerTheory contains the definitions for Euclidean div and mod, let's use that instead of redefining these operators in HolSmtTheory. commit b5d90204b1ce9320ca8724010b116b3961fed5b1 Author: someplaceguy <[email protected]> Date: Thu Mar 14 12:01:51 2024 +0000 Add Euclidean div and mod, plus some num/int theorems commit eddeef51c3ad8343b9642a3fcbe8191ea23d97bd Author: someplaceguy <[email protected]> Date: Thu Mar 14 02:22:04 2024 +0000 HolSmt: fix workaround for extra hypothesis in proof replay The previously-implemented workaround might have an issue where if Z3 introduces an hypothesis of the form `P = P` but then *doesn't* forget to discharge it, we might fail to replay the `lemma` proof rule because we avoided adding an assumption. Instead, this commit fixes the workaround so that we remove the extra hypothesis at the end of the proof replay procedure, i.e. only when we are sure that Z3 *did* forget to discharge the hypothesis. commit a30d4a4276ab4e511759b5aa37aaf4c668695649 Author: someplaceguy <[email protected]> Date: Tue Mar 12 14:55:08 2024 +0000 HolSmt: update documentation commit 4b596255753e0c57fab7f386fd567a2f9e45c47c Author: someplaceguy <[email protected]> Date: Tue Mar 12 12:10:32 2024 +0000 HolSmt: try harder to replay arithmetic proof steps This commit adds some tactics which help prove some arithmetic proof steps that intLib.{ARITH,COOPER}_TAC can't deal with. These are basically some workarounds for: https://github.com/HOL-Theorem-Prover/HOL/issues/1207 This allows us to enable proof replay for the remaining arithmetic test cases that didn't already have proof replay enabled, with the exception of the very last test case (because we can't replay nonlinear arithmetic proof steps). That said, I don't expect these workarounds to be very reliable. Ideally, it would be better to improve HOL4's linear arithmetic decision procedures. commit 1a0145aa2b01864cf7dacae4af64f50ff9ae1bc2 Author: someplaceguy <[email protected]> Date: Tue Mar 12 10:39:08 2024 +0000 HolSmt: merge z3_lemma_arith and z3_rewrite's arith Since these two decision procedures need to handle the same kind of terms (including smtdiv / smtmod rewrites), this commit merges them. commit d3c92d76638ab87aa0abd0666222c22b0bde2d0b Author: someplaceguy <[email protected]> Date: Tue Mar 12 09:43:12 2024 +0000 HolSmt: work around Z3 bug in `hypothesis` proof rule In some proof certificates, Z3 emits a `hypothesis` inference rule without discharging it later with a `lemma` rule. This causes some proofs to fail at the end of the proof replay procedure, because they end up containing an extra hypothesis. Fortunately, so far all such undischarged hypothesis rules were of the form `p = p`, so for now we can easily work around this issue by creating such theorems without adding an assumption. This workaround allows us to enable proof replay for 5 more self-tests. commit ec98ab611a41c3643d00986ccc55ced58d9049ef Author: someplaceguy <[email protected]> Date: Tue Mar 12 09:25:57 2024 +0000 HolSmt: work around NotFound exn in ARITH_PROVE This commit contains a workaround for the following issue: https://github.com/HOL-Theorem-Prover/HOL/issues/1209 commit e903f05e498126f29731c7ee5203da5f0f268de9 Author: someplaceguy <[email protected]> Date: Tue Mar 12 09:13:39 2024 +0000 HolSmt: enable the remaining div and mod tests commit 19c2c262c61864d0b7d6063c67891e2a38ab19c8 Author: someplaceguy <[email protected]> Date: Tue Mar 12 06:53:15 2024 +0000 HolSmt: implement `iff-false` Z3 proof rule commit c4c184a688f131ecc3f3216887f2d9cbb94838f5 Author: someplaceguy <[email protected]> Date: Tue Mar 12 05:57:33 2024 +0000 HolSmt: major fixes for Z3 replay of `th_lemma_arith` rule The `th_lemma_arith` was running into several issues. The following changes were made: 1. The `generalize_ite` procedure was removed, since the arithmetic decision procedures can handle `if ... then ... else ...` now. It was causing replay failures because some terms were not provable unless the decision procedures could inspect the `if` bodies. 2. The arithmetic decision procedures don't understand `smtdiv` and `smtmod`; so before proving the term, we now rewrite it with the definitions of these functions. 3. A workaround was also implemented for some instances of the following issue: https://github.com/HOL-Theorem-Prover/HOL/issues/1207 Namely, the integer decision procedures cannot decide some terms containing `ABS` and `Num`, so we rewrite them when possible. commit 8d6e54bd5aa0bab7ab96a77a066672babfdd80c8 Author: someplaceguy <[email protected]> Date: Tue Mar 12 03:58:22 2024 +0000 HolSmt: parse `div0` and `mod0` in Z3 proofs Unfortunately, these operators don't seem to be documented. However, from a quick reading of the Z3 source code, it seems that they seem to be similar to `div` and `mod`, but they seem to be used to indicate that Z3 can't prove that the divisor is non-zero. commit a2f47a923362ee9cf921731134034340380e3b82 Author: someplaceguy <[email protected]> Date: Tue Mar 12 03:38:41 2024 +0000 HolSmt: enable DIV tests commit 4ca0db5b762ee280b8ee0376e6923aec666e81cd Author: someplaceguy <[email protected]> Date: Tue Mar 12 03:16:29 2024 +0000 HolSmt: add some arithmetic theorems SMT_NUM_ADD and SMT_NUM_SUB were meant to be used in place of INT_ADD and INT_NUM_SUB for optimization reasons. However, this causes a regression in proof replay in one of the self-tests. Since this regression is not straightforward to fix, these theorems are not being used yet. NUM_OF_INT was also added to the default set of theorems since it helps solve some `num`-related goals. commit 48b39a8f98f4f0c5a6aaffc7dd340835935e7034 Author: someplaceguy <[email protected]> Date: Tue Mar 12 03:04:16 2024 +0000 HolSmt: fix hang in arith Z3 proof replay The previous workaround for ARITH_PROVE failing to prove some terms changed the `th_lemma_arith` proof handler to use COOPER_PROVE instead. However, COOPER_PROVE sometimes is too slow and appears to hang when replaying some Z3 proofs. This commit changes the `th_lemma_arith` handler to first try ARITH_PROVE which is much faster, and only if it fails, then try COOPER_PROVE. commit dba3657acffebd68ad8fb34d0ab8569e0fb9c9e8 Author: someplaceguy <[email protected]> Date: Sun Mar 10 01:07:10 2024 +0000 HolSmt: add support for div and mod commit 7ef04d38a121fd9082a8652ae6150ce1abc95366 Author: someplaceguy <[email protected]> Date: Mon Mar 11 02:40:48 2024 +0000 HolSmt: fix `let ... and ...` SMT-LIB translation The SMT-LIB term translator couldn't handle parallel definitions properly. This commit fixes that. commit 8605071187e3c0ef971cddef84a24a5675764bfa Author: Chun Tian (binghe) <[email protected]> Date: Wed Mar 27 14:28:02 2024 +1100 [combin] Add one more theorem: EXTENSIONAL_RESTRICTION commit cf6d9862da6d2e4f113bfe7148118503c570658c Author: Chun Tian (binghe) <[email protected]> Date: Fri Mar 22 15:08:21 2024 +1100 EXTENSIONAL and RESTRICTION ported from HOL-Light commit 65f2a59f55f5c55ae2c6ce188a1269e1618bd94b Author: Magnus Myreen <[email protected]> Date: Sat Apr 6 05:27:22 2024 +0200 Generate small numbers only once in thm/Compute.sml commit 7ec599db91151b3c6a6bad0b092bdc1c2c7d50ea Author: Magnus Myreen <[email protected]> Date: Sat Apr 6 05:20:15 2024 +0200 Make Thm.compute do more earlier commit 22300a65f94b48536e01a7e9be50b927e85d0d19 Author: Magnus Myreen <[email protected]> Date: Sat Apr 6 03:41:58 2024 +0200 Make Thm.compute accumulate thm tags commit 738ed9400c7d3bc2ca6b7cda70f65773c83b4c93 Author: Michael Norrish <[email protected]> Date: Wed Apr 3 20:36:49 2024 +1100 Fix bug in SWAP_EXISTS_CONV (manifested in Cooper's d.p. in integer) commit a925fed59eccd6d257c42d2a5d88d2ce7429f6ed Author: Magnus Myreen <[email protected]> Date: Thu Apr 4 04:23:03 2024 +0200 Make sure "cv_" appears before theory name prefix commit 2875e0cbdd7bba461a4d893a0a38f34c73a63b2c Author: Magnus Myreen <[email protected]> Date: Thu Apr 4 04:08:47 2024 +0200 Use cv_trans instead of cv_trans_pre in a few places commit 4d623c3e0ede1afab926cae9fe4680475b8d6584 Author: Magnus Myreen <[email protected]> Date: Thu Apr 4 04:08:00 2024 +0200 Avoid name clashes in cv_transLib commit 3fa79893fb30ba3225975b8ef528ca4d2c6ecf55 Author: Michael Norrish <[email protected]> Date: Wed Apr 3 14:06:41 2024 +1100 Fix INCLUDES line in src/finite_maps/Holmakefile Knock-on from a4d582152a. Thanks to Chun Tian for report of problem. commit 798d323a82e0c012aa981b4d9978d6642fef9034 Author: Michael Norrish <[email protected]> Date: Tue Apr 2 14:22:55 2024 +1100 Test-case tweaks given 9edfb8164e5c04ac ASCII arrows get replaced by \HOLTokenMap{} and some linebreaking changes as a result also. commit a4d582152a96076cd18c887a983f5be0224c7806 Author: Michael Norrish <[email protected]> Date: Tue Apr 2 11:39:33 2024 +1100 Handle |-> token for TeX p/printing in finite_maps better Now the same TeX notation is used for the |-> in “:'a |-> 'b” and in “f(| k |-> v |)”. commit 9edfb8164e5c04aca3d09b71f3c736c1225ddc20 Author: Michael Norrish <[email protected]> Date: Tue Apr 2 11:38:51 2024 +1100 Get TeX p/printing to do nice LaTeX for types (arrows and Greek) commit 13c94a2f00a7c40cae8579e5b4eb9f451ade661f Author: Magnus Myreen <[email protected]> Date: Sun Mar 31 07:35:16 2024 +0200 Avoid [] pretty printing as epsilon commit b53822e18dcfb4bf9d4267afa9a310614bf5b940 Author: Hrutvik Kanabar <[email protected]> Date: Tue Mar 26 14:12:37 2024 +0000 Some fixes - Unicode violations - Missing `INCLUDES` in `Holmakefile` - Update a `README` commit b7051d3b53f58d5f4db06272afbafdbfa9bebdc8 Author: Michael Norrish <[email protected]> Date: Tue Mar 26 18:07:31 2024 +1100 Provide TeX notations for function update syntax commit f57070d427868aa51f38b29eabf4353ceabb7a5e Author: Hrutvik Kanabar <[email protected]> Date: Sat Mar 23 14:20:23 2024 +0000 Sketch `cv_transLib` entry in Description commit ddf702878b2cc0ea0830738ee0631b0e72da57e9 Author: Hrutvik Kanabar <[email protected]> Date: Sat Mar 23 14:20:23 2024 +0000 Pass through docfiles commit 9e8cb30bf8756b6c7bae0ca2ba897b7344026c18 Author: Michael Norrish <[email protected]> Date: Sat Mar 23 10:36:42 2024 +1100 Start of some work on "algebras as types" Starting with the base of the algebra pyramid keeps things simpler, and will hopefully allow the technology to be worked out and polished. commit 55c6eca980922f551a135a65496c07ec603fd52e Author: Michael Norrish <[email protected]> Date: Fri Mar 22 20:12:04 2024 +1100 Implement a xfer_fwd_tac for transferLib commit ce133ee32087143dbe61b7c81c4948f10d82c7da Author: Michael Norrish <[email protected]> Date: Fri Mar 22 20:11:09 2024 +1100 Define extend fn to extend a monoid's carrier to all of type commit 44bb8cea085b9993b36885f7a2f69610063c6b86 Author: Michael Norrish <[email protected]> Date: Fri Mar 22 20:10:04 2024 +1100 Mention polarity search in release notes This was implemented in PR #1208 commit 591cfcf1656d67f4d28fce86854c800f22f93956 Author: Michael Norrish <[email protected]> Date: Fri Mar 22 20:07:23 2024 +1100 Fix another bug in Omega d.p. Thanks to someplaceguy for reporting these. Progress of sorts with github issue #1207 commit e546764f153c268543103c60ed61bd9941768e05 Author: Chun Tian (binghe) <[email protected]> Date: Wed Mar 20 14:57:39 2024 +1100 Speedup examples/probability building process commit f97f4ffa7db4a7929723438df248a180bd1b435b Author: Chun Tian (binghe) <[email protected]> Date: Tue Mar 19 11:50:05 2024 +1100 Fixed TeX munge outputs of NegInf (extreal) commit 6252f430c58963c182efc0f3e6cc690dc3631a4a Author: Chun Tian (binghe) <[email protected]> Date: Mon Mar 18 23:22:55 2024 +1100 Added algebra_finite_subsets_imp_sigma_algebra, etc. commit 3c8a6cb48a5cb437988afe41dc0933480fcc5ee4 Author: Chun Tian (binghe) <[email protected]> Date: Mon Mar 18 11:59:01 2024 +1100 Minor fix & updates to probability materials commit dd274cc494f343180dc4e8406d93ee7b96e46f63 Author: Chun Tian (binghe) <[email protected]> Date: Thu Mar 14 19:05:56 2024 +1100 [lambda] Boehm_out_lemma (Proposition 10.3.7 (i) [1, p.248]) commit 5a607569d2a0fd0abe15add18996f1709aff1241 Author: Eric Hall <[email protected]> Date: Tue Mar 19 22:58:46 2024 +1100 Allowing user to choose between positive polarity matching and negative polarity matching by providing a prefix argument commit 1321abd20bd7245fec98bb448f98ed33795bc861 Author: Eric Hall <[email protected]> Date: Tue Mar 19 18:26:30 2024 +1100 Fixing issue where unicode symbol was being used where this was not permitted commit 7ac3d89624a1d893b31a32fdefe1180b06916031 Author: Eric Hall <[email protected]> Date: Mon Mar 11 22:27:18 2024 +1100 Fixing silly bug which prevented polarity search from working commit a8f13229afe5e39ca05f37815bbb6d3ae4a6c35c Author: Eric Hall <[email protected]> Date: Sat Mar 9 22:33:50 2024 +1100 adding code to use hotkey to search for theorems based on terms in premises and conclusions commit d6cc90288bffbd6a1807302e291235ac866a2efb Author: Eric Hall <[email protected]> Date: Sat Mar 9 20:49:06 2024 +1100 Writing code to allow theorems to be searched based on what terms appear as premises or conclusions to those theorems, rather than simply testing whether a particular term is present in the theorem anywhere. commit 1a1b46d9be426307029882cb1e3bcfbdaf0c43a1 Author: Michael Norrish <[email protected]> Date: Tue Mar 19 17:28:48 2024 +1100 Handle natural number subtraction under & better in int d.p.'s Addresses a couple of cases from github issue #1207 commit 5788053992c2aff5952489f5367121dac8cdbff2 Author: Michael Norrish <[email protected]> Date: Tue Mar 19 15:55:05 2024 +1100 Fix handling of Num in line with its new semantics Possible because of 55230652bbe9 Closes #1203 commit 671b4b712f9e860a558393b4b0c6a15e3a52a754 Author: Chun Tian (binghe) <[email protected]> Date: Wed Mar 13 22:41:51 2024 +1100 Updated HOL Description with higher mathematics contents promoted to chapter level commit 9ac238fdf4bfbd20dd4c90d977c3f4a137c36287 Author: Matthew Richards <[email protected]> Date: Wed Mar 13 14:19:18 2024 +1100 Add clearer error on double implication in inductive definitions Previously a more cryptic error would be raised here; now it should be diagnosed that conjunctions are to be used instead. commit 424be5497b74891ab006a67b5c809a3943d23305 Author: Hrutvik Kanabar <[email protected]> Date: Sun Mar 17 17:54:04 2024 +0000 Add a random sptree lemma commit 23a41fbb4d1034fcddba3dd82ce9c4fbde586b7e Author: Magnus Myreen <[email protected]> Date: Sun Mar 17 22:38:36 2024 +0100 Make cv_*trans_rec return unit commit e63c18572a7d5796e1f419c6d870d0e5a5391416 Author: Magnus Myreen <[email protected]> Date: Sun Mar 17 21:36:28 2024 +0100 Write some doc files for cv_trans functions commit e8de5684760f5fb51d4cae7992feb21bdf016e40 Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 16:55:23 2024 +0000 Add a cv docfile Co-authored-by: Magnus Myreen <[email protected]> commit 5188e60f751cd0e86ec4a231d93cba6ad07391f9 Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 10:53:10 2024 +0000 Expand on cv text in `next-release.md` Co-authored-by: Magnus Myreen <[email protected]> commit 0b944581367edae0f87be5e61e2684d2117f6ed4 Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 16:00:42 2024 +0000 Copy over cv translator examples from CakeML/cakeml#985 commit 542fc78f63b80f52c5b0ce357999104b98a5344f Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 15:55:55 2024 +0000 Delete old cv examples commit fc160dde5f557fa0a0c7def21fd5722bee09c08e Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 15:53:00 2024 +0000 Move some theorems to appropriate theories commit 02e4b212fe47e70e04b32f4d982d239b9ca1b5ce Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 10:53:10 2024 +0000 Move a few cv functions Co-authored-by: Magnus Myreen <[email protected]> commit a7babafe2cfc2ac6ec2e583e5cd8ad411a13a62f Author: Hrutvik Kanabar <[email protected]> Date: Fri Mar 15 10:53:10 2024 +0000 Copy over cv translator work from CakeML/cakeml#985 Co-authored-by: Magnus Myreen <[email protected]> commit 9f96ab9d68b28bc65d470932346d72c4a17ac605 Author: Michael Norrish <[email protected]> Date: Fri Mar 15 16:39:35 2024 +1100 Document DB.selectDB; tweak doc file for DB.find commit cf3fab22e341c82a4dc94399c23c0fc062b65816 Author: Michael Norrish <[email protected]> Date: Fri Mar 15 15:47:38 2024 +1100 Clean up some doc-files; preferring not to use alpha --> bool syntax This is a little confusing for new users who may not appreciate that types are typically obtained by calling the parser (“:...” syntax). commit 01d5d9a7f4d32b0d18003f956a45f226dd43badd Author: Michael Norrish <[email protected]> Date: Fri Mar 15 15:45:12 2024 +1100 Fix bug in holfoot that let its parser get contaminated by others' In particular, its parsing referred to term_grammar() which let changes in other theories (in this case HolSmt) contaminate its namespace. Fix is to make sure its parsing is done with holfootTheory.holfoot_grammars (its own relatively fixed grammars). commit e8b31786a24bec9b97777b614e69d558846a3b60 Author: Michael Norrish <[email protected]> Date: Thu Mar 14 17:32:11 2024 +1100 Fix bug in Omega test Make slight changes to code along the way; making it easier to see state of dictionary that is used internally. Bug was in call to one_var_analysis where a stale map variable (ptree) was used, when the correct parameter was (pt) which was the continuation's parameter. Add a number of test-cases, all of which are probably more or less equivalent. Thanks to someplaceguy for the bug report! Closes #1209 commit b9bd54bebaa9faa2874dc92ee667d148f2770384 Author: Michael Norrish <[email protected]> Date: Wed Mar 13 16:15:15 2024 +1100 Upgrade integer DP testing code to use testutils commit eeb10e889818e1f3fbaafad49ecb125de7280bda Author: Michael Norrish <[email protected]> Date: Wed Mar 13 16:13:03 2024 +1100 Fix a bug in PIntMap.size commit 29e263e51c911f218102d767840a34bc7cb1b2df Author: Chun Tian (binghe) <[email protected]> Date: Sat Mar 9 13:51:02 2024 +1100 Better statements of Boehm_transform_exists_lemma commit 5314eb3da47a6c5426a1337fdf960a150fc1f650 Author: Chun Tian (binghe) <[email protected]> Date: Fri Mar 8 15:43:32 2024 +1100 [lambda] Boehm_transform_exists_lemma (Lemma 10.3.6 (ii) [1, p.247]) commit fbaa3a988821dfedb37377814ae537fd6855e3ab Author: someplaceguy <[email protected]> Date: Sat Mar 9 19:27:13 2024 +0000 HolSmt: fix Z3 proof replay of `asserted` proof rules This commit contains both a fix and a workaround for replaying `asserted` proof rules. The fix consists in disabling the `pp.simplify_implies` Z3 parameter. This parameter controls whether the Z3 AST pretty-printer does some simplifications when printing the proof and is enabled in Z3 by default. However, these simplifications can effectively mangle the terms in the `(asserted ...)` inference rules, which means they will not match the terms that were actually asserted in the input file (i.e. the terms in the assumptions of the goal). Therefore, these mangled terms would cause proof replay to fail in some cases. Unfortunately, in currently released versions of Z3 (i.e. 4.12.6 and earlier) it is not actually possible to disable `pp.simplify_implies` when printing the proof. A fix for this issue was submitted as the following PR: https://github.com/Z3Prover/z3/pull/7157 To mitigate this parameter not currently working in Z3, a workaround was also implemented which tries to remove mangled asserted statements, which would end up as extra hypotheses in the final theorem. This workaround has been confirmed to work in Z3 v4.12.6 as well as Z3 v2.19. Since this issue has been fixed, we can now enable two more self-tests. commit c725a1a758751f12ac9feaeaa7cd80fc9cd5c8c9 Author: someplaceguy <[email protected]> Date: Sat Mar 9 04:41:09 2024 +0000 HolSmt: add four rewrite theorems for Z3 proof replay This allows us to enable proof replay for one more self-test. Another self-test was added that exercises at least two of these theorems that the other self-tests don't. commit 823e6496a30dd2c10dd5456295223e575887563b Author: someplaceguy <[email protected]> Date: Sat Mar 9 04:22:55 2024 +0000 HolSmt: replay `sk` inference rule in Z3 proofs This proof handler implements the following inference rules: |- ~(!x. P x y) <=> ~(P (sk y) y) |- (?x. P x y) <=> P (sk y) y The implementation is complicated due to the need to create the Skolem terms and due to the need for higher-order matching. Z3 proof replay was enabled for one more self-test. commit f3f5e21f6213772ce745ccf70c06d442f34b04a5 Author: someplaceguy <[email protected]> Date: Fri Mar 8 23:19:51 2024 +0000 HolSmt: fix `elim-unused` proof rule to work w/ `exists` quantifiers The `elim-unused` rule handler could only handle `forall` quantifiers. However, Z3 also uses it for `exists` quantifiers. This commit makes the handler work with both quantifiers, including when they are interspersed with each other. This fix is necessary for replaying an `elim-unused` rule in the Z3 proof for the following self-test: ?x. x = x This commit also enables proof replay for the above self-test, since the proof can now be fully reconstructed. commit c488a6c95a397379f61bf76b997fb31356d5b83e Author: someplaceguy <[email protected]> Date: Fri Mar 8 22:38:06 2024 +0000 HolSmt: fix `quant-intro` proof rule to work w/ `exists` quantifiers The `quant-intro` rule handler could only handle `forall` quantifiers. However, Z3 also uses it for `exists` quantifiers. This commit makes the handler work with both quantifiers, including when they are interspersed with each other. This fix is necessary for replaying a `quant-intro` rule in the Z3 proof for the following self-test: ?x. x = x commit 466d6c224a2db972ce86d30971e8fcbd788162a6 Author: someplaceguy <[email protected]> Date: Thu Mar 7 21:46:30 2024 +0000 HolSmt: build an smtheap This reduces the loading time of HolSmtLib from around 42s to about 5s (on my laptop). commit 68f30d60a1586c1fb27f53effa6e12adc98023b9 Author: someplaceguy <[email protected]> Date: Wed Mar 6 02:12:10 2024 +0000 HolSmt: enable Z3 proof replay of `num` self-tests Due to all the recent fixes and improvements in the Z3 proof certificate parser and replay code, we can now replay these proofs correctly, so we can enable these tests (for Z3 v4 only, as these Z3 v2 proof certificates contain undeclared terms that we are not able to replay). commit 9f055e47f9a0dca4f65fa8e073275f3c16ba9c23 Author: someplaceguy <[email protected]> Date: Thu Mar 7 14:57:47 2024 +0000 HolSmt: work around Z3 quant-inst proof rule issue This is a quick workaround for the following Z3 issue: https://github.com/Z3Prover/z3/issues/7154 commit 194563d5a050d34234035a7246502661adc7bb06 Author: someplaceguy <[email protected]> Date: Wed Mar 6 17:13:44 2024 +0000 HolSmt: work around ARITH_PROVE bug This is a workaround for the following issue: https://github.com/HOL-Theorem-Prover/HOL/issues/1203 When the above issue is fixed, this commit can be reverted. commit 7724583437d63ccc97dca5d13b4719e5e4cc35cd Author: someplaceguy <[email protected]> Date: Wed Mar 6 01:16:58 2024 +0000 HolSmt: parse `proof-bind` rules in Z3 proofs These appear not to have any semantic value despite the Z3 v4.12.4 source code implying that it either introduces lambda abstractions or `forall` quantifiers, depending on the interpretation. commit 355248c6a3d8dfb4f5021c84a43934b6f477dae2 Author: someplaceguy <[email protected]> Date: Wed Mar 6 00:54:26 2024 +0000 HolSmt: replay `refl` inference rule in Z3 proofs Also, parse the `~` operator when used as `equivalence modulo naming`. commit 1c6e508280b9602107f0cd0ffde897bcd4f1526b Author: someplaceguy <[email protected]> Date: Tue Mar 5 21:40:20 2024 +0000 HolSmt: parse `lambda` binders in Z3 proofs These seem to be a local declaration of variable names+types that apparently are meant to be interpreted as free variables in the enclosed term. Note that these `lambda` binders should only be parsed when parsing Z3 proof certificates, as the SMT-LIB language as specified in the current 2.6 version of the standard doesn't actually have these binders and we don't want to parse identifiers coincidentally named `lambda` as these special binders in this case. We take advantage of the previously-implemented parser parametrization to determine whether `lambda` binders should be parsed or not. commit 193cfe1c332b2859b4fbb354d4141b27af61fb6c Author: someplaceguy <[email protected]> Date: Tue Mar 5 19:57:12 2024 +0000 HolSmt: parse nested `let` bindings in Z3 proofs Z3 proof certificates contain `let` definitions nested within other `let` definitions. The SMT-LIB parser would parse these as HOL4 `let` terms, but we don't actually want to create those. Instead, we just need to bind the definitions to the names. Since the SMT-LIB parser can now be parametrized by `let` handling functions, we make use of this new functionality to parse `let` terms differently when parsing Z3 proof certificates. commit 16e6d9426c44fb142c0715da0c0c54551966b69c Author: someplaceguy <[email protected]> Date: Tue Mar 5 19:21:30 2024 +0000 HolSmt: parametrize the SMT-LIB parser by `let` handling functions The SMT-LIB term parser and Z3 proof certificate parser are similar in most ways, but they need to handle `let` terms differently. To avoid having to duplicate a significant portion of the parser, this commit parametrizes the SMT-LIB parser so that it can handle these `let` expressions differently based on parser handling functions that are passed by the caller of the term parser. In this commit, only the SMT-LIB version of the `let` handling functions are implemented, so it doesn't change how the parsers work yet. However, in a subsequent commit, the Z3 proof parser will use this new functionality to parse the proof certificates correctly. commit 0fb203fde51288bd3536e1e430d4c38098cf3441 Author: someplaceguy <[email protected]> Date: Wed Mar 6 00:35:53 2024 +0000 HolSmt: rename nums -> indices Since indices are not necessarily numerals now, it's probably better to rename these function arguments. commit 9640aeee1360656094181e76ccc68c4047de0642 Author: someplaceguy <[email protected]> Date: Sun Mar 3 17:30:30 2024 +0000 HolSmt: replay `quant-inst` rule in Z3 v4 proofs It is an inference rule that creates the following proof: ------------------------------------------ QUANT_INST [u1,...,un] |- ~(!x1...xn. t) \/ t[u1/x1]...[un/xn] commit f51b78741843c13b151b2b2cac1f06c5890af64a Author: someplaceguy <[email protected]> Date: Sat Mar 2 18:06:20 2024 +0000 HolSmt: parse indexed identifiers' indices as terms Prior to SMT-LIB 2.5, the indices of indexed identifiers could only be numerals. In SMT-LIB 2.5 and later, identifiers can be indexed not just with numerals but also with symbols. This was implemented in commit 8a2e9bc97c2955bdbda0bceb90948e87a92f5c22 However, the `quant-inst` inference rule in Z3 v4 proofs can contain arbitrary terms as its indices, as seen in this example: ((_ quant-inst (v12 v17) (v11 v17 ?x304)) ...) In order to add support for this rule in a follow-up commit, the SMT-LIB parser was changed to support arbitrary terms as indices in term identifiers (but not type identifiers). This should be a superset of what SMT-LIB allows, which should be fine because we don't need to implement a strict parser. However, Z3 v2 proof certificates contain inference rules such as the following: (_ |th-lemma| arith farkas -41/42 -1) In particular, `-41/42` and `-1` are not valid SMT-LIB terms. We used to parse this successfully because we allowed arbitrary strings as indices, but since we are trying to parse terms, this is now being rejected by the parser. Due to this regression, proof replay for some test cases was disabled for Z3 v2 (but they are still enabled for Z3 v4). commit 043537b739e1b3a8de19e345630b587e1660d1d0 Author: someplaceguy <[email protected]> Date: Sat Mar 2 01:54:38 2024 +0000 HolSmt: replay `mp~` proof rule in Z3 v4 proofs It's the same as the `Thm.EQ_MP` inference rule in HOL4. commit 8932bbb3a745a23bb867f80badfa011d2dd04a9f Author: someplaceguy <[email protected]> Date: Sat Mar 2 01:48:39 2024 +0000 HolSmt: print invalid proofterms It's quite useful when debugging the usage of a proofterm that is missing in the proofterm dictionary. commit c49e07bd42564a2cf9e267cb819d8a30eecc7b95 Author: someplaceguy <[email protected]> Date: Sat Mar 2 01:12:11 2024 +0000 HolSmt: replay the `nnf-neg` and `nnf-pos` proof rules These should create proofs of negative normal form (NNF) steps. For the initial implementation, we rely on `metisLib.METIS_TAC` to find these proofs. If it becomes a bottleneck, a more specialized implementation could be developed. commit 7aea54b0522c7fa3a6ab8a78ab57b706514e498f Author: someplaceguy <[email protected]> Date: Thu Feb 29 21:46:40 2024 +0000 HolSmt: make sure `let` definitions use unique names in Z3 proofs This commit adds code to check that Z3 proof certificates use unique names in `let` definitions. This is especially important to check now that some `let` definitions in Z3 proofs don't have its scope open until the end of the proof. commit cc836c940b3592b1044cf2f9e4d45edefe75fc8a Author: someplaceguy <[email protected]> Date: Thu Feb 29 01:04:12 2024 +0000 HolSmt: hoist Z3 proof `let` parsing into separate function This is the initial step in making the proof certificate parsing more flexible. It doesn't change how the proof certificates are parsed, but this small refactoring will make it easier to make some improvements that are planned for later. commit 72c0ab0a6835be5f76e503275f8b8169204571b5 Author: someplaceguy <[email protected]> Date: Wed Feb 28 23:41:00 2024 +0000 HolSmt: disable Z3 v2 on failing test cases Z3 v2 is now failing in some tests due to fallout of some previous changes that were needed to add support for the `num` type. There are 2 root causes for these failures: 1. Z3 v2 doesn't know about the integer `ABS` function. We used to rewrite the conclusion of the goal with the `INT_ABS` theorem but this is not needed when using modern SMT solvers because SMT-LIB supports `ABS` natively. 2. Due to changes in how some goals are passed onto the SMT solvers, Z3 v2 is now generating proof certificates with some undeclared and untyped terms which we are not able to reconstruct. While I don't yet see a compelling reason to actively remove support for Z3 v2 (since support for Z3 v4 is mostly a superset of our support for Z3 v2), I don't see a compelling reason for adding v2-specific workarounds either, due to how old it is and due to it being unsupported for many years already. This commit adds new `thm_Z3_v4` and `thm_Z3p_v4` functions which only run the test cases if Z3 is configured and is version 4. These new functions are used in the test cases which succeed with Z3 v4 but not with Z3 v2. commit 62097611c00799ddef1f5c78fa710a90fb4af811 Author: someplaceguy <[email protected]> Date: Sun Feb 25 22:07:24 2024 +0000 HolSmt: add support for the `num` type This commit adds support for SMT solvers to reason about the `num` type by providing them with some theorems which allow them to convert `num` operations into integer operations which they natively support. Specifically, it adds to the proving context (as assumptions) theorems for the following conversions between `num` terms and integers: * `num` literals [INT_OF_NUM] * `SUC`, i.e. ``&SUC n <=> &n + 1i`` [INT] * `num` equality [INT_INJ] * `num` inequalities [INT_LE, INT_LT, GREATER_DEF, GREATER_EQ] * Non-negativity of `num` terms [INT_POS] * `num` addition and multiplication [INT_ADD, INT_MUL] * MIN and MAX [INT_MIN, INT_MAX] This is not an exhaustive list of all the theorems that will be needed to reason about the `num` type or even just `num` arithmetic, but it does allow Z3 to solve all the `num`-related self-tests, with the notable exception of DIV and MOD operators. To fix the latter, we will need to add support for integer division and mod first. Unfortunately cvc5 cannot solve a few of the `num` tests and the Z3 proof reconstruction fails for almost all `num` tests, although this is not due to unsoundness in `num` support, but rather because the Z3 proof certificates for these goals are more complex and use new proof syntax and rules which we do not support yet (this will be fixed later). There is another unfortunate regression: adding these theorems to the context prevents SMT solvers from giving `sat` answers. In fact, this happens even when just one theorem is added to the goal as an assumption (`integerTheory.INT`, specifically, which is needed to reason about `SUC`), regardless of which goal we try to prove. Fortunately, this does not prevent them from answering `unsat`. Since in the self-tests we do rely on `sat` answers to validate unprovable goals, the tests which expect a `sat` answer were modified to temporarily disable the inclusion of the above theorems while performing…
Hi,
The abstract algebra work (under
examples/algebra
, etc.) by (Joseph) Hing-Lun Chan is an important contribution to HOL4. The present huge PR moves this work (up to monoid, only) into the core library, under a new directory "src/algebra".Perhaps It's impossible to review all code changes (50k+ additions, 58k- deletions) in the commits. Below is just a summary of ideas behind those changes:
examples/algebra/lib
andexamples/fermat
:numberTheory
: theorems about numbers that involves new definitions beyondarithmeticTheory
,gcdTheory
, etc.combinatoricsTheory
: definitions and theorems usually considered as part of "Combinatorics" (e.g. thenecklaceTheory
and the originalcombinatoricsTheory
underexamples/fermat
)primeTheory
: theorems about prime numbers which depends oncombinatoricsTheory
.monoidTheory
is added as a combined theory of all theories underexamples/algebra/monoid
except for the one depending on real numbers.real_algebraTheory
is added (under "src/real") with the monoid of real numbers (for now). This theory will collect other algebra objects based on real numbers, in the future.arithmetic
,divides
,gcd
,gcdset
,list
,rich_list
,pred_set
,bag
, etc.) to enrich these theories with more supporting theorems. In the future, we should keep polishing the new theories under "src/algebra" to move some small theorems to upstream theories.SNOC_LAST_FRONT
(⊢ ∀l. l ≠ [] ⇒ SNOC (LAST l) (FRONT l) = l
)recently added intorich_listTheory
but is conflict with another similar theorem fromexamples/algebra
. I give the algebra materials the higher priority and renamed my theorem toSNOC_OF_LAST_FRONT
. (NOTE: this change is now reverted. The similar theorem from algebra materials is now calledSNOC_LAST_FRONT'
, which is used only 4 times inpolyWeakScript.sml
.)SQ = \n. n * n
,HALF
,TWICE
, etc.) which I consider not very necessary. I have changed them totemp_overload_on()
without touching their proofs.Once the present PR gets merged, the next steps would be moving also the
groupTheory
andringTheory
, etc. (after theory combinations) to "src/algebra", and then start making connections to other existing theories.Chun Tian